
\section{Themes, Goals and Topics of the Workshop}

\subsection{Goals}

If we generically consider a model transformation as an algorithm describing specific model manipulations, then testing it or proving some of its properties can be envisaged.
However, unlike reactive systems---for which many verification techniques have been proposed---a model transformation performs particular computations where:
(1) it typically operates on models, thus on data at a high-level of abstraction rich in semantics and
(2) from a pragmatic point of view, often only the initial input and the final output is of interest and none of the intermediate steps matters.
These are primary fundamental differences between model transformations verification and classical verification of programs written in general-purpose programming languages.
A particular subject of interest for VOLT is the fact that model transformations are used to perform specific computations in the context of MDD, such as model refinement, refactoring, translation, synthesis, simulation, or synchronization~\cite{Mens2006}.
In this sense, we feel that useful verification techniques for model transformations can and possibly should be specific to these activities.

\subsection{Topics}

To discuss these problems, we would like to invite submissions related to the following topics:
%
\begin{itemize}
  \item Application of formal verification, theorem proving, model checking or testing to model transformation;
  \item Verification techniques dedicated to model transformation;
  \item Taxonomies of techniques for model transformation verification;
  \item Properties relevant to specific model transformations;
  \item Verification of model transformations expressed in languages such as: ATL, QVT, TGG, VIATRA, Kermeta, Epsilon, etc.
  \item Verification of domain-specific model transformations~\cite{Kuhne2010}, in contrast to general-purpose transformations;
  \item Case studies and experience reports;
  \item Tools and automation.
\end{itemize}


\subsection{Relevance to ECMFA}

Many members of the ECMFA community are of course practitioners of MDD and have also proposed techniques for MDD, both for testing and formal verification.
Many software intensive industries (\eg automotive, avionics, telephony) have nowadays standardized the use of MDD and incorporated the use of models in their development
processes, with a decrease in manufacturing costs (see~\cite{citeulike:9594369} for a well-known example).
Despite interest of the industry in model transformations, the technology is still too academical and not sufficiently standardized.
In particular, studying techniques to raise the level of confidence in a model transformation or ensure that a model transformation is correct in a certain context is certainly the next logical step to raise industrial interest.
Such a study would solidify and promote the whole area of research in model transformation and favor its adoption in real world projects.
Certainly last year's edition was a big success having attracted to the discussions many new participants and stimulated the field of transformation verification by having a forum dedicated to this topic.  

The specific contribution of VOLT is to allow an open discussion space that combines solid theoretical work with practical on-the-field experience in verification of model transformations. As such, it represents a valuable and complementary resource for a scientific conference like ECMFA.
